The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(x, nil)) → x
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
empty(nil) → true
empty(cons(n, x)) → false
head(cons(n, x)) → n
tail(nil) → nil
tail(cons(n, x)) → x
sort(x) → sortIter(x, nil)
sortIter(x, y) → if(empty(x), x, y, append(y, cons(min(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → sortIter(replace(min(x), head(x), tail(x)), z)

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
eq(s(n), s(m)) →⁺ eq(n, m)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [n / s(n), m / s(m)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)